Nuprl Lemma : exp_zero_q
11,40
postcript
pdf
e
:
.
e
0 = 1
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
1
,
|
r
|
,
x
:
A
.
B
(
x
)
,
r
n
Lemmas
crng
wf
,
qrng
wf
,
rng
nexp
zero
origin
e:
. e 
0 = 1 
e:. e 0 = 1 T+*>x:A. B(x) n